COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	hill[f86,jmc]		Logical hill climbing
C00004 ENDMK
C⊗;
hill[f86,jmc]		Logical hill climbing

	It is very straightforward to write a block stacking program,
but it's not so easy to see how to get a general prover to solve the
problem from axioms.  It seems likely that the program is easy to
write because we immediately conjecture a function measuring progress.
A function measuring progress should have the following properties.

1. If the function keeps increasing, we win in a reasonable time.

2. The function of state or partial state is easy to compute.

3. It doesn't take too much look-ahead to find a way to improve.

Remark: I guess we actually only need a binary predicate of
improvement.

It helps to have a  worse  predicate or a  lose  predicate.  It
also helps to have a plausible move generator.

In the blocks world a position  P2  is better than  P1 if
P2  resembles  P1,  except that yet another block is in final position.
Also if a block that has to be moved has fewer on top of it and no
blocks that have to be moved have more on top of them.  These are
sufficient in a blocks world with a large table.